//package ca.shojaei.mini_sat;
//import java.util.Stack;
//import java.util.regex.*;
//
//import BinTree.PNode;
//import ca.shojaei.mini_sat.Parser.ParseError;
//
//
///*		Some definitions
//
//	    <expression>  ::=  [ "!" | "e@" | "a@" ] <factor> [["!"] [ "&" | "|" | "e@" | "a@" |
//	    "eU" | "aU"] <factor> ]
//
//	    <factor>  ::=  <char>  |  "(" <expression> ")"
// */
//
//
//
////-------------------- Classes for Expression Trees ------------------------------
//
//
//abstract class ExpNode {
//}
//
//class ConstNode extends ExpNode {
//	// An expression node that holds a character only.
//	char p;  // The character.
//	ConstNode(char val) {
//		// Construct a ConstNode containing the specified number.
//		p = val;
//	}
//	char value() {
//		// The value of the node is the number that it contains.
//		return p;
//	}
//}
//
//class OpNode extends ExpNode {
//
//	String op;        // The operator.
//	ExpNode left;   // The expression for its left operand.
//	ExpNode right;  // The expression for its right operand.
//	OpNode(String op, ExpNode left, ExpNode right) {
//		// Construct a BinOpNode containing the specified data.
//		this.op = op;
//		this.left = left;
//		this.right = right;
//	}
//} 
//
//class UnaryMinusNode extends ExpNode {
//	// An expression node to represent a unary minus operator.
//	ExpNode operand;  // The operand to which the unary minus applies.
//	UnaryMinusNode(ExpNode operand) {
//		// Construct a UnaryMinusNode with the specified operand.
//		this.operand = operand;
//	}
//}
//
//class OpAndSize{
//
//	public Clause op;
//	public int size;
//
//	public OpAndSize(){}
//}
//
//class OpAndString{
//
//	public Clause op;
//	public String left;
//	public String right;
//
//	public OpAndString(){}
//}
//
//
//public class Parser2 {
//	static class ParseError extends Exception {
//		// Represents a syntax error found in the user's input.
//		ParseError(String message) {
//			super(message);
//		}
//	} // end nested class ParseError
//
//
//	static OpAndString FindMainOperator(String input){
//		OpAndString os = new OpAndString();
//		int i = 0;//MAKE SURE WE DON'T PASS AN INITIAL '('
//
//		boolean negation;  // True if there is a leading minus sign.
//		negation = false;
//		if (input.charAt(i) == '!') {
//			negation = true;
//			i++;
//		}		
//		OpAndSize clause;
//		//Determine if the main operator is unary
//		int operator = isOperator(input.charAt(i), input.charAt(i +1));
//		if(operator == 1 || operator == 2){
//			clause = getOperator(input.charAt(i), input.charAt(i+1));
//			if(negation){
//				clause.op.setNegated(true);
//			}
//			os.op = clause.op;
//			os.left = input.substring(i+ clause.size);
//			os.right = "";
//		}
//		//The following is for a binary operator
//		else{
//			boolean done = false;
//			int leftB = -1;
//			while(!done){		
//				if(leftB == 0){
//					done = true;
//					break;
//				}
//				if(input.charAt(i) == '('){
//					if(leftB == -1)
//						leftB = 1;
//					else 
//						leftB ++;
//				}
//				else if(input.charAt(i) == ')')
//					leftB --;
//				i++;
//			}
//			if(done){
//				os.left = input.substring(0, i);//TODO: FIX THIS SO IT RETURNS NO BRACKETS
//			}
//			clause = getOperator(input.charAt(i), input.charAt(i+1));
//			if(negation){
//				clause.op.setNegated(true);
//			}
//			os.op = clause.op;
//			os.right = input.substring(i+ clause.size);
//		}
//		return os;
//	}
//
//	static boolean StringHasOperator(String inputString){
//
//		if(inputString.contains("&") || inputString.contains("|") || inputString.contains("e@") ||
//				inputString.contains("a@") || inputString.contains("eU") || inputString.contains("aU"))
//			return true;
//		else
//			return false;
//	}
//
//	static Clause parseString(String inputString, int pos, Clause clause, boolean right) throws ParseError{
//
//		/*<expression>  =  [ "!" | "e@" | "a@" ] <factor> [ [ "&" | "|" | "e@" | "a@" |
//		"eU" | "aU" | "!" ] <factor> ]
//	   <factor>  =  <char>  |  "(" <expression> ")"                                            	    
//		 */
//		//TODO: Pass to the function the first position after the first parenthesis!
//		Clause child = new Clause();
//		if(!StringHasOperator(inputString)){
//			boolean negation;  // True if there is a leading ! sign.
//			negation = false;
//			if (inputString.charAt(pos) == '!') {
//				negation = true;
//				pos++;
//			}
//			child = new Item(String.valueOf(inputString.charAt(pos)));
//			if(negation)
//				child.setNegated(true);
//
//			if(right)
//				clause.setRight(child);
//			else
//				clause.setLeft(child);
//		}
//		else{
//			OpAndString ops = FindMainOperator(inputString);
//			child = ops.op;
//
//			Clause left = parseString(ops.left, 0,child,false);
//			Clause rightC = null;
//			if(!ops.right.equals(""))
//				rightC = parseString(ops.right, 0,child,true);
//
//			child.setLeft(left);
//			child.setRight(rightC);
//
//			if(right)
//				clause.setRight(child);
//			else
//				clause.setLeft(child);
//		}
//		return child;
//	}
//
//	static boolean notSpecial(char c){
//		if(c != '!' || c != '&' || c!= '(' || c!= ')')
//			return true;
//		else
//			return false;
//	}
//
//	static String removeBlanks(String input){
//
//		char[] myString = input.toCharArray();
//		int index = input.lastIndexOf(' ');
//		int i = 0;
//		char[] result = new char[input.length()];
//
//		while(index >= 0 ){
//
//			while(i<index){
//				result[i] = myString[i];
//				i++;
//			}
//			if(i == index){
//				while(i < myString.length - 1){
//					result[i] = myString[i+1];
//					i++;
//				}
//			}
//			index = input.lastIndexOf(' ');
//			i = 0;
//			myString = result;
//		}
//
//		return String.copyValueOf(result);
//	}
//
//	static String cleanString(String input){
//		
//		int i = 0;
//		int end = 0;
//		while(input.charAt(i) == '(')
//			i++;
//		end = i;
//		while(input.charAt(i) != ')')
//			end++;
//		return input.substring(i, end);
//	}
//	static int isOperator(char a, char b){
//
//		if((a == '&') || (a == '|'))
//			return 1;
//		else if((a == 'e' || a == 'a') && (b == '@' || b == 'U'))
//			return 2;
//		else 
//			return 0;
//	}
//
//	static OpAndSize getOperator(char a, char b){
//
//		String op = "";
//		if((a == '&') || (a == '|'))
//			op = String.valueOf(a);
//		if((a == 'e' || a == 'a') && (b == '@' || b == 'U')){
//			op = String.valueOf(a);
//			op.concat(String.valueOf(b));
//		}
//		return getOperatorAndSizeClass(op);
//	}
//
//	static OpAndSize getOperatorAndSizeClass(String op){
//
//		OpAndSize opS = new OpAndSize();
//		opS.op = null;
//		opS.size = 1;
//		if(op.equals("&")){
//			opS.op = new And();
//		}
//		if(op.equals("|")){
//			opS.op = new Or();
//		}
//		opS.size = 2;
//		if(op.equals("eU")){
//			opS.op = new ExistsUntil();
//		}
//		if(op.equals("e@")){
//			opS.op = new ExistsNext();
//		}
//		if(op.equals("aU")){
//			opS.op = new ForAllUntil();
//		}
//		if(op.equals("a@"))
//			opS.op = new ForAllNext();
//
//		return opS;
//	}
//
//	static String getClassOperator(String op){
//
//		if(op.equals("&"))
//			return "And";
//		if(op.equals("|"))
//			return "Or";
//		if(op.equals("eU"))
//			return "ExistsUntil";
//		if(op.equals("e@"))
//			return "ExistsNext";
//		if(op.equals("aU"))
//			return "ForAllUntil";
//		if(op.equals("a@"))
//			return "ForAllNext";    		
//		else
//			return " ";
//	}
//
//
//	static Clause getClass(String op){
//
//		if(op.equals("&"))
//			return new And();
//		if(op.equals("|"))
//			return new Or();
//		if(op.equals("eU"))
//			return new ExistsUntil();
//		if(op.equals("e@"))
//			return new ExistsNext();
//		if(op.equals("aU"))
//			return new ForAllUntil();
//		if(op.equals("a@"))
//			return new ForAllNext();    		
//		else
//			return null;
//	}
//	/* TODO:Error handling
// static boolean rightFormat(String input){
//
//	 for()
//	 return false;
//
// }*/
//}//End of Parser Class
//

